Establish RED-4: observation-blind realization checking - #14

Purpose

Establish the next machine-checked negative result after GREEN-3.

GREEN-3 checks:

• semantic identity -> target resource;
• semantic value -> raw representation;
• target trace -> protocol transition model.

RED-4 asks whether that is enough to establish that the intended device effect was actually observed.

It is not.

Witness

Both outcomes contain the exact same GREEN-3-valid execution:

resource       = 0x20
raw write      = 250
protocol trace = enter-config
                 issue-write
                 observe-ACK
                 exit-config

Only the post-execution observation changes:

reference observation = some 250
mutated observation   = none

Machine-checked result

reference.execution = mutated.execution
reference.observation != mutated.observation

GREEN3(reference) = true
GREEN3(mutated)   = true

This establishes:

a valid modeled realization is not the same thing as an observed semantic effect.

Claim boundary

This PR does not yet claim that raw observation 250 proves the intended semantic effect. The current theory cannot state that relation. That missing relation is precisely RED-4.

GREEN-4 constraint

The next step must distinguish the outcomes without:

• trusting a realization-generated success flag;
• treating ACK alone as proof of semantic effect;
• embedding target-specific observation details in the target-neutral contract;
• claiming simulator or physical-device conformance prematurely.

Payload-to-trace linkage also remains explicitly open; RED-4 does not hide or solve it.